T:Type, R:(TT).
(x, y:T. Dec(R(x,y)))
 Linorder(T;x,y.R(x,y))
 (a, b:T. (strict_part(x,y.R(x,y);a;b))  R(b,a)) 

latex

Up	rel 1, rel 1
Definitions	x,y. t(x;y), t  T, strict_part(x,y.R(x;y);a;b), x(s1,s2), P  Q, , x:A. B(x), P  Q, P & Q, A, P  Q, AntiSym(T;x,y.R(x;y)), Trans(T;x,y.E(x;y)), Refl(T;x,y.E(x;y)), Connex(T;x,y.R(x;y)), Order(T;x,y.R(x;y)), Linorder(T;x,y.R(x;y)), False, P  Q, Dec(P)
Lemmas	decidable wf, linorder wf, not wf